/-
Copyright (c) 2020 Kim Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module

public import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
public import Mathlib.CategoryTheory.Limits.Types.Colimits
public import Mathlib.Logic.Function.Coequalizer
public import Mathlib.Tactic.CategoryTheory.Elementwise

/-!
# Coequalizers in Type

The coequalizer of a pair of maps `(f, g)` from `X` to `Y`
is the quotient of `Y` by `∀ x : Y, f x ~ g x`

-/

@[expose] public section

universe v u

open CategoryTheory Limits

namespace CategoryTheory.Limits.Types

variable {X Y Z : Type u} (f g : X ⟶ Y)

/-- Show that the quotient by the relation generated by `f(x) ~ g(x)`
is a coequalizer for the pair `(f, g)`.
-/
def coequalizerColimit : Limits.ColimitCocone (parallelPair f g) where
  cocone :=
    Cofork.ofπ (Function.Coequalizer.mk f g) (funext fun x => Function.Coequalizer.condition f g x)
  isColimit :=
    Cofork.IsColimit.mk _
      (fun s ↦ Function.Coequalizer.desc f g s.π s.condition)
      (fun _ ↦ rfl)
      (fun _ _ hm ↦ funext (fun x ↦ Quot.inductionOn x (congr_fun hm)))

/-- If `π : Y ⟶ Z` is a coequalizer for `(f, g)`, and `U ⊆ Y` such that `f ⁻¹' U = g ⁻¹' U`,
then `π ⁻¹' (π '' U) = U`.
-/
theorem coequalizer_preimage_image_eq_of_preimage_eq (π : Y ⟶ Z) (e : f ≫ π = g ≫ π)
    (h : IsColimit (Cofork.ofπ π e)) (U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) : π ⁻¹' (π '' U) = U := by
  have lem : ∀ x y, Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U) := by
    rintro _ _ ⟨x⟩
    change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
    rw [H]
  have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U := by
    aesop (add safe constructors _root_.Equivalence)
  ext
  constructor
  · rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]
    rintro ⟨y, hy, e'⟩
    dsimp at e'
    replace e' :=
      (mono_iff_injective
            (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
        inferInstance e'
    exact (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact e'))).mp hy
  · exact fun hx => ⟨_, hx, rfl⟩

/-- The categorical coequalizer in `Type u` is the quotient by `f g ~ g x`. -/
noncomputable def coequalizerIso : coequalizer f g ≅ Function.Coequalizer f g :=
  colimit.isoColimitCocone (coequalizerColimit f g)

@[elementwise (attr := simp)]
theorem coequalizerIso_π_comp_hom :
    coequalizer.π f g ≫ (coequalizerIso f g).hom = Function.Coequalizer.mk f g :=
  colimit.isoColimitCocone_ι_hom (coequalizerColimit f g) WalkingParallelPair.one

@[elementwise (attr := simp)]
theorem coequalizerIso_quot_comp_inv :
    ↾Function.Coequalizer.mk f g ≫ (coequalizerIso f g).inv = coequalizer.π f g :=
  rfl

end CategoryTheory.Limits.Types
